Nuprl Lemma : R-da_wf
0,22
postcript
pdf
R
:Realizer,
i
:Id. R-da(
R
;
i
)
k
:Knd fp
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
R-da(
R
;
i
)
,
Prop
,
x
.
t
(
x
)
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
,
y
,
z
,
u
,
v
,
w
.
t
(
x
;
y
;
z
;
u
;
v
;
w
)
,
x
,
y
,
z
,
w
,
v
.
t
(
x
;
y
;
z
;
w
;
v
)
,
x
(
s1
,
s2
,
s3
,
s4
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
a
,
b
,
c
,
d
,
e
,
f
)
,
x
(
s1
,
s2
,
s3
,
s4
,
s5
)
,
x
(
s
)
Lemmas
es
realizer
ind
wf
,
fpf
wf
,
Knd
wf
,
fpf-empty
wf
,
fpf-join
wf
,
Kind-deq
wf
,
es
realizer
wf
,
Id
wf
,
IdLnk
wf
,
ifthenelse
wf
,
eq
id
wf
,
fpf-single
wf
,
decl-state
wf
,
decl-type
wf
,
lsrc
wf
,
lnk-decl
wf
,
locl
wf
origin
x:A. B(x), t 
T, R-da(R;i), Prop, 
x. t(x), x,y,z,w. t(x;y;z;w), x,y,z. t(x;y;z), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w,v. t(x;y;z;w;v), x(s1,s2,s3,s4), x(s1,s2,s3), x(a,b,c,d,e,f), x(s1,s2,s3,s4,s5), x(s)
Type